perm filename BLISET.AX[226,JMC] blob
sn#005398 filedate 1972-06-18 generic text, type T, neo UTF8
00100 GIVEAX(SITDEF,(∀ S)(∀ Y)(∀ X)(X ε SIT(Y,S) ≡ SITTING(X,Y,S)));
00200
00300 GIVEAX(SITSET,(∀ S)(∀ Y)(ISSET SIT(Y,S)));
00400
00500 GIVEAX(EXTENSIONALITY,(∀ U)(∀ V)(ISSET U ∧ ISSET V ⊃
00600 ((∀ X)(XεU ≡ XεV) ⊃ U=V)));
00700
00800 GIVEAX(SITTING,(∀ S)(∀ X)(∀ Y)(SITTING(X,Y,S) ≡
00900 (AT(X,Y,S)∧¬(X=ROBOT)∧¬HOLDING(X,S))));
01000
01100 GIVEAX(HELDSET,(∀ S)(ISSET HELD S));
01200
01300 GIVEAX(HELDDEF, (∀ S)(∀ X)(HOLDING(X,S)⊃HELD(S)=UNITSET(X)));
01400
01500 GIVEAX(HELDDEF2,(∀ S)((∀ X)(¬HOLDING(X,S))⊃(HELD(S)=NULLSET)));
01600
01700 GIVEAX(NULLSET,ISSET NULLSET);
01800
01900 GIVEAX(NULL1,(∀ X)(¬(XεNULLSET)));
02000
02100 GIVEAX(UNITSET,(∀ X)(∀ Y)(YεUNITSET(X)≡(Y=X)));
02200
02300 GIVEAX(UNIONSET,(∀ X)(∀ Y)(ISSET X ∧ ISSET Y ⊃ ISSET UNION(X,Y)));
02400
02500 GIVEAX(UNION,(∀ X)(∀ Y)(∀ Z)(ZεUNION(X,Y)≡ZεX∨ZεY));
02600
02700 END;